T:Type, L:(T List), i,j:int_seg(0; ||L||).
(i < j)  sublist(T; cons(L[i]; cons(L[j]; [])); L) 

latex

Definitions	False, A, t  ...$L, ge(i; j), A  B, suptype(S; T), subtype(S; T), prop{i:l}, t  T, Y, increasing(f; k), P  Q, x:A. B(x), sublist(T; L1; L2), P  Q, ||as||, x:A. B(x), ff, tt, guard(T), sq_type(T), (i = j), if b then t else f fi , i <z j, b, i z j, nth_tl(n;as), hd(l), l[i], tl(l), int_seg(i; j), lelt(i; j; k), P  Q, decidable(P)
Lemmas	non neg length, length cons, length nil, select wf, increasing wf, length wf1, int seg wf, eq int wf, ifthenelse wf, decidable int equal